Sets as Types

sets as types(型としての集合)

集合と型とは同一と見なせる

HoTTの本から持ってきた、下記の表が型と集合の関係はどんな対応かがわかりやすい

$ \begin{array}{c|c|c|c} 型(\mathrm{Types}) & 論理(\mathrm{Logic}) & 集合(\mathrm{Sets}) & ホモトピー \\ \hline A & 命題 & 集合 & 空間 \\ a: A & 証明 & 元 & 点 \\ B(x) & 述語 & 集合の族 & ファイブレーション \\ b(x) : B(x) & \mathrm{条件付き証明} & 元の族 & \mathrm{切断} \\ \bm{0, 1} & \bot , \top & \varnothing , \{ \varnothing \} & \varnothing, * \\ A + B & A \lor B & \mathrm{非交和} & 余直積 \\ A \times B & A \land B & 組の集合 & 積の空間 \\ A \to B & A \implies B & 関数の集合 & 関数空間 \\ \sum_{(x:A)}B(x) & \exist_{x:A} B(x) & \mathrm{直和} & \mathrm{全空間} \\ \prod_{(x:A)}B(x) & \forall_{x:A} B(x) & 積 & 切断の空間 \\ \mathrm{Id}_A & 等号\ = & \lbrace (x, x) | x \in A \rbrace & 道空間A^I \end{array}

ref: "Homotopy Type Theory Univalent Foundations of Mathematics" Table 1: Comparing points of view on type-thoretic operations (P11)

抽出

$ \begin{array}{c|c} 型(\mathrm{Types}) & 集合(\mathrm{Sets}) \\ \hline A & 集合A \\ a: A & 元a \\ B(x) & 集合の族\{A_i\} \\ b(x) : B(x) & 元の族 \\ \bm{0} & \varnothing \\ \bm{1} & \{ \varnothing \} \\ A + B & \mathrm{非交和}A \sqcup B \\ A \times B & 組の集合 \\ A \to B & 関数の集合 \\ \sum_{(x:A)}B(x) & \mathrm{直和} \\ \prod_{(x:A)}B(x) & 積 \\ \mathrm{Id}_A & \lbrace (x, x) | x \in A \rbrace \end{array}

確認用

Q. set as types